f1(0) -> s1(0)
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
↳ QTRS
↳ DependencyPairsProof
f1(0) -> s1(0)
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
F1(s1(s1(x))) -> F1(f1(s1(x)))
F1(s1(s1(x))) -> F1(s1(x))
f1(0) -> s1(0)
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F1(s1(s1(x))) -> F1(f1(s1(x)))
F1(s1(s1(x))) -> F1(s1(x))
f1(0) -> s1(0)
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F1(s1(s1(x))) -> F1(s1(x))
Used ordering: Polynomial Order [17,21] with Interpretation:
F1(s1(s1(x))) -> F1(f1(s1(x)))
POL( 0 ) = 0
POL( s1(x1) ) = x1 + 1
POL( F1(x1) ) = x1
POL( f1(x1) ) = 2
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
f1(0) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
F1(s1(s1(x))) -> F1(f1(s1(x)))
f1(0) -> s1(0)
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F1(s1(s1(x))) -> F1(f1(s1(x)))
POL( 0 ) = max{0, -2}
POL( s1(x1) ) = x1 + 2
POL( F1(x1) ) = 2x1
POL( f1(x1) ) = 2
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))
f1(0) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f1(0) -> s1(0)
f1(s1(0)) -> s1(0)
f1(s1(s1(x))) -> f1(f1(s1(x)))